﻿// Autore: Alessio Parma

using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
using System.Diagnostics.Contracts;
using System.Linq;
using RecipesManager.Data.Properties;

namespace RecipesManager.Data
{
    public static class ErrorMessages
    {
        public const string AlreadyUsedCategoryName = "00";
        public const string AlreadyUsedGuestName = "01";
        public const string AlreadyUsedIngredientName = "02";
        public const string AlreadyUsedRecipeName = "03";
        public const string AlreadyUsedShopName = "04";
        public const string InvalidQbMeasure = "05";
        public const string InvalidHours = "06";
        public const string InvalidMinutes = "07";
        public const string InvalidServings = "08";
        public const string NegativeQuantity = "09";
        public const string NegativeOrZeroQuantity = "10";
        public const string ZeroLengthDescription = "11";
        public const string ZeroLengthName = "12";

        internal const string IdNotExisting = "Non esiste alcuna entità avente ID specificato.";
        internal const string NameExisting = "Esiste già un'entità avente nome specificato.";
        internal const string NameNotExisting = "Non esiste alcuna entità avente nome specificato.";

        public static readonly IDictionary<string, string> Messages = new Dictionary<string, string>();

        static ErrorMessages()
        {
            Messages[AlreadyUsedCategoryName] = "Esiste già una categoria avente il nome specificato.";
            Messages[AlreadyUsedGuestName] = "Esiste già un ospite avente il nome specificato.";
            Messages[AlreadyUsedIngredientName] = "Esiste già un ingrediente avente il nome specificato.";
            Messages[AlreadyUsedRecipeName] = "Esiste già una ricetta avente il nome specificato.";
            Messages[AlreadyUsedShopName] = "Esiste già un negozio avente il nome specificato.";
            Messages[InvalidQbMeasure] = "Impossibile aggiungere un ingrediente avente \"Quanto Basta\" come unità di misura.";
            Messages[InvalidHours] = "Le ore sono comprese tra 0 e 72.";
            Messages[InvalidMinutes] = "I minuti sono compresi tra 0 e 59.";
            Messages[InvalidServings] = "Le porzioni sono comprese tra 1 e 50.";
            Messages[NegativeQuantity] = "La quantità deve essere zero o un numero positivo.";
            Messages[NegativeOrZeroQuantity] = "La quantità deve essere un numero positivo.";
            Messages[ZeroLengthDescription] = "Il campo descrizione non può essere lasciato vuoto.";
            Messages[ZeroLengthName] = "Il campo nome non può essere lasciato vuoto.";
        }
    }

// ReSharper disable ClassNeverInstantiated.Global
    public sealed class DataException : Exception
// ReSharper restore ClassNeverInstantiated.Global
    {
        public DataException(string message) : base(ExtractMessage(message))
        {
        }

        static string ExtractMessage(string message)
        {
            var lastBlank = message.LastIndexOf(' ');
            var code = message.Substring(lastBlank + 1);
            return ErrorMessages.Messages[code];
        }
    }

    [ContractClassFor(typeof(IEntity))]
    abstract class EntityContract : IEntity
    {
        #region IEntity Members

        public abstract int Id { get; }

        #endregion
    }

    [ContractClassFor(typeof(INamedEntity))]
    abstract class NamedEntityContract : INamedEntity
    {
        #region INamedEntity Members

        public abstract int Id { get; }
        public abstract string Name { get; }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(!string.IsNullOrEmpty(Name));
        }
    }

    [ContractClassFor(typeof(IEntities<>))]
    abstract class EntitiesContract<TEntity> : IEntities<TEntity>
        where TEntity : class, IEntity
    {
        #region IEntities<TEntity> Members

        public abstract IEnumerator<TEntity> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract TEntity LastAdded { get; }
        public abstract IEnumerable<TEntity> Unordered { get; }

        public TEntity this[int id]
        {
            get
            {
                Contract.Requires(Contains(id), ErrorMessages.IdNotExisting);
                Contract.Ensures(Contract.Result<TEntity>() != null);
                Contract.Ensures(Contract.Result<TEntity>().Id == id);
                Contract.Ensures(Contract.OldValue(Count) == Count);
                return default(TEntity);
            }
        }

        public bool Contains(int id)
        {
            Contract.Ensures(Contract.OldValue(Count) == Count);
            return default(bool);
        }

        public void Remove(int id)
        {
            Contract.Requires(Contains(id), ErrorMessages.IdNotExisting);
            Contract.Ensures(!Contains(id));
            Contract.Ensures(Contract.OldValue(Count) == Count + 1);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Count >= 0);
            Contract.Invariant(Unordered != null);
        }
    }

    [ContractClassFor(typeof(INamedEntities<>))]
    abstract class NamedEntitiesContract<TEntity> : INamedEntities<TEntity>
        where TEntity : class, INamedEntity
    {
        #region INamedEntities<TEntity> Members

        public abstract IEnumerator<TEntity> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract TEntity LastAdded { get; }
        public abstract IEnumerable<TEntity> Unordered { get; }
        public abstract TEntity this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);

        public TEntity this[string name]
        {
            get
            {
                Contract.Requires(Contains(name), ErrorMessages.NameNotExisting);
                Contract.Ensures(Contract.Result<TEntity>() != null);
                Contract.Ensures(Contract.Result<TEntity>().Name == name.ToKey());
                Contract.Ensures(Contract.OldValue(Count) == Count);
                return default(TEntity);
            }
        }

        public bool Contains(string name)
        {
            Contract.Requires(name != null);
            Contract.Requires<DataException>(name.Length > 0, ErrorMessages.ZeroLengthName);
            Contract.Ensures(Contract.OldValue(Count) == Count);
            return default(bool);
        }

        public void Remove(string name)
        {
            Contract.Requires(Contains(name), ErrorMessages.NameNotExisting);
            Contract.Ensures(!Contains(name));
            Contract.Ensures(Count == Contract.OldValue(Count) - 1);
        }

        #endregion
    }

    [ContractClassFor(typeof(ILink<>))]
    abstract class LinkContract<TEntity> : ILink<TEntity>
        where TEntity : class, INamedEntity
    {
        #region ILink<TEntity> Members

        public abstract IEnumerator<TEntity> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract TEntity LastAdded { get; }
        public abstract IEnumerable<TEntity> Unordered { get; }
        public abstract TEntity this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract TEntity this[string name] { get; }
        public abstract bool Contains(string name);
        public abstract void Remove(string name);

        public abstract INamedEntities<TEntity> Entities { get; }

        public TEntity Add(string name)
        {
            Contract.Requires(Entities.Contains(name), ErrorMessages.NameNotExisting);
            Contract.Requires(!Contains(name), ErrorMessages.NameExisting);
            ContractAbbreviators.EnsureValidNamedEntitiesAdd(this, name);
            Contract.Ensures(LastAdded.Equals(Contract.Result<TEntity>()));
            Contract.Ensures(Contract.Result<TEntity>().Name == name.ToKey());
            Contract.Ensures(Count == Contract.OldValue(Count) + 1);
            return default(TEntity);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Entities != null);
        }
    }

    [ContractClassFor(typeof(IRating<,>))]
    abstract class RatingContract<TEntity, TRating> : IRating<TEntity, TRating>
        where TEntity : class, INamedEntity
        where TRating : struct
    {
        #region IRating<TEntity,TRating> Members

        public abstract int Id { get; }
        public abstract string Name { get; }

        public abstract TEntity Entity { get; }
        public abstract TRating Rating { get; }

        public void Update(TRating rating)
        {
            Contract.Ensures(Rating.Equals(rating));
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Entity != null);
            Contract.Invariant(Entity.Id == Id && Entity.Name == Name);
        }
    }

    [ContractClassFor(typeof(IRatings<,>))]
    abstract class RatingsContract<TEntity, TRating> : IRatings<TEntity, TRating>
        where TEntity : class, INamedEntity
        where TRating : struct
    {
        #region IRatings<TEntity,TRating> Members

        public abstract IEnumerator<IRating<TEntity, TRating>> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IRating<TEntity, TRating> LastAdded { get; }
        public abstract IEnumerable<IRating<TEntity, TRating>> Unordered { get; }
        public abstract IRating<TEntity, TRating> this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract IRating<TEntity, TRating> this[string id] { get; }
        public abstract bool Contains(string id);
        public abstract void Remove(string id);

        public abstract INamedEntities<TEntity> Entities { get; }

        public IRating<TEntity, TRating> Add(string name, TRating rating)
        {
            Contract.Requires(Entities.Contains(name), ErrorMessages.NameNotExisting);
            Contract.Requires(!Contains(name), ErrorMessages.NameExisting);
            ContractAbbreviators.EnsureValidNamedEntitiesAdd(this, name);
            Contract.Ensures(LastAdded.Equals(Contract.Result<IRating<TEntity, TRating>>()));
            Contract.Ensures(Contract.Result<IRating<TEntity, TRating>>().Name == name.ToKey());
            Contract.Ensures(Contract.Result<IRating<TEntity, TRating>>().Rating.Equals(rating));
            Contract.Ensures(Count == Contract.OldValue(Count) + 1);
            return default(IRating<TEntity, TRating>);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Entities != null);
        }
    }

    [ContractClassFor(typeof(IOtherRating<,>))]
    abstract class OtherRatingContract<TEntity, TRating> : IOtherRating<TEntity, TRating>
        where TEntity : class, INamedEntity
        where TRating : struct
    {
        #region IOtherRating<TEntity,TRating> Members

        public abstract TEntity Entity { get; }
        public abstract int Id { get; }
        public abstract string Name { get; }
        public abstract TRating Rating { get; }

        public void Update(TRating rating)
        {
            Contract.Ensures(Rating.Equals(rating));
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Entity != null && Name != null);
            Contract.Invariant(Entity.Id == Id && Entity.Name == Name);
        }
    }

    [ContractClassFor(typeof(ICategory))]
    abstract class CategoryContract : ICategory
    {
        #region ICategory Members

        public abstract int Id { get; }
        public abstract string Name { get; }
        public abstract bool Equals(ICategory other);

        public abstract ILink<ICategory> Children { get; }
        public abstract IEnumerable<IGuest> GuestIntolerances { get; }
        public abstract IEnumerable<IOtherRating<IGuest, FoodRating>> GuestRatings { get; }
        public abstract ILink<IIngredient> Ingredients { get; }
        public abstract ILink<ICategory> Parents { get; }

        public void Update(string name)
        {
            ContractAbbreviators.RequireUnusedName(Name, name, Manager.Categories, ErrorMessages.AlreadyUsedCategoryName);
            Contract.Ensures(Name == name.ToKey() && Manager.Categories.Contains(Name) &&
                             (Contract.OldValue(Name) == name.ToKey() ||
                              !Manager.Categories.Contains(Contract.OldValue(Name))));
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Children != null && Children.All(c => c.Parents.Contains(Id)));
            Contract.Invariant(Parents != null && Parents.All(p => p.Children.Contains(Id)));
            Contract.Invariant(GuestIntolerances != null && GuestRatings != null);
            Contract.Invariant(GuestIntolerances.All(g => g.CategoryIntolerances.Contains(Id)));
            Contract.Invariant(GuestRatings.All(g => g.Entity.CategoryRatings.Contains(Id)));
        }
    }

    [ContractClassFor(typeof(ICategories))]
    abstract class CategoriesContract : ICategories
    {
        #region ICategories Members

        public abstract IEnumerator<ICategory> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract ICategory LastAdded { get; }
        public abstract IEnumerable<ICategory> Unordered { get; }
        public abstract ICategory this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract ICategory this[string id] { get; }
        public abstract bool Contains(string id);
        public abstract void Remove(string name);

        public ICategory Add(string name)
        {
            Contract.Requires<DataException>(!Contains(name), ErrorMessages.AlreadyUsedCategoryName);
            ContractAbbreviators.EnsureValidNamedEntitiesAdd(this, name);
            return default(ICategory);
        }

        #endregion
    }

    [ContractClassFor(typeof(IEvent))]
    abstract class EventContract : IEvent
    {
        #region IEvent Members

        public abstract int Id { get; }
        public abstract bool Equals(IEvent other);

        public abstract DateTime? Date { get; }
        public abstract bool HasEnded { get; }
        public abstract IGuestParticipations Guests { get; }
        public abstract string Name { get; }
        public abstract string Notes { get; }
        public abstract IRecipesServings Recipes { get; }

        public void Close()
        {
            Contract.Requires(!HasEnded);
            Contract.Ensures(HasEnded);
        }

        public void Update(string name, string notes, DateTime? date)
        {
            Contract.Requires(name != null && notes != null);
            Contract.Requires<DataException>(name.Length > 0, ErrorMessages.ZeroLengthName);
            Contract.Ensures(Name == name && Notes == notes && Date == date);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Name != null && Notes != null);
            Contract.Invariant(Guests != null && Recipes != null);
            Contract.Invariant(Guests.All(g => g.Guest.EventsParticipations.Any(e => e.Id == Id)));
            Contract.Invariant(Recipes.All(r => r.Recipe.Events.Any(e => e.Id == Id)));
        }
    }

    [ContractClassFor(typeof(IEvents))]
    abstract class EventsContract : IEvents
    {
        #region IEvents Members

        public abstract IEnumerator<IEvent> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IEvent LastAdded { get; }
        public abstract IEnumerable<IEvent> Unordered { get; }
        public abstract IEvent this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);

        public IEvent Add(string name, string notes, DateTime? date)
        {
            Contract.Requires(notes != null);
            ContractAbbreviators.RequireValidName(name);
            ContractAbbreviators.EnsureValidEntitiesAdd(this);
            Contract.Ensures(Contract.Result<IEvent>().Name == name);
            Contract.Ensures(Contract.Result<IEvent>().Notes == notes);
            Contract.Ensures(Contract.Result<IEvent>().Date == date);
            return default(IEvent);
        }

        #endregion
    }

    [ContractClassFor(typeof(IGuest))]
    abstract class GuestContract : IGuest
    {
        #region IGuest Members

        public abstract int Id { get; }
        public abstract string Name { get; }
        public abstract bool Equals(IGuest other);

        public abstract ILink<ICategory> CategoryIntolerances { get; }
        public abstract IRatings<ICategory, FoodRating> CategoryRatings { get; }
        public abstract IEnumerable<IEvent> EventsParticipations { get; }
        public abstract ILink<IIngredient> IngredientIntolerances { get; }
        public abstract IRatings<IIngredient, FoodRating> IngredientRatings { get; }
        public abstract IRatings<IGuest, GuestRating> GuestRatings { get; }
        public abstract ILink<IGuest> GuestRelationships { get; }
        public abstract IEnumerable<IOtherRating<IGuest, GuestRating>> OtherGuestRatings { get; }
        public abstract string Notes { get; }
        public abstract IRatings<IRecipe, FoodRating> RecipeRatings { get; }
        public abstract IRecipeStats RecipeStats { get; }

        public void Update(string name, string notes)
        {
            Contract.Requires(name != null && notes != null);
            ContractAbbreviators.RequireUnusedName(Name, name, Manager.Guests, ErrorMessages.AlreadyUsedGuestName);
            Contract.Ensures(Name == name.ToKey() && Notes == notes);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(CategoryIntolerances != null && CategoryRatings != null);
            Contract.Invariant(CategoryIntolerances.All(c => c.GuestIntolerances.Any(g => g.Id == Id)));
            Contract.Invariant(CategoryRatings.All(c => c.Entity.GuestRatings.Any(g => g.Id == Id)));
            Contract.Invariant(IngredientIntolerances != null && IngredientRatings != null);
            Contract.Invariant(IngredientIntolerances.All(i => i.GuestIntolerances.Any(g => g.Id == Id)));
            Contract.Invariant(IngredientRatings.All(i => i.Entity.GuestRatings.Any(g => g.Id == Id)));
            Contract.Invariant(GuestRatings != null && OtherGuestRatings != null && GuestRelationships != null);
            Contract.Invariant(GuestRatings.All(g => g.Entity.OtherGuestRatings.Any(gg => gg.Id == Id)));
            Contract.Invariant(OtherGuestRatings.All(g => g.Entity.GuestRatings.Any(gg => gg.Id == Id)));
            Contract.Invariant(GuestRelationships.All(g => g.GuestRelationships.Contains(Id)));
            Contract.Invariant(RecipeRatings != null && RecipeStats != null);
            Contract.Invariant(RecipeRatings.All(r => r.Entity.GuestRatings.Any(g => g.Id == Id)));
            Contract.Invariant(EventsParticipations != null && Notes != null);
            Contract.Invariant(EventsParticipations.All(e => e.Guests.Contains(Id)));
        }
    }

    [ContractClassFor(typeof(IGuests))]
    abstract class GuestsContract : IGuests
    {
        #region IGuests Members

        public abstract IEnumerator<IGuest> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IGuest LastAdded { get; }
        public abstract IEnumerable<IGuest> Unordered { get; }
        public abstract IGuest this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract IGuest this[string id] { get; }
        public abstract bool Contains(string id);
        public abstract void Remove(string name);

        public IGuest Add(string name, string notes)
        {
            Contract.Requires(notes != null);
            Contract.Requires<DataException>(!Contains(name), ErrorMessages.AlreadyUsedGuestName);
            ContractAbbreviators.EnsureValidNamedEntitiesAdd(this, name);
            Contract.Ensures(Contract.Result<IGuest>().Notes == notes);
            return default(IGuest);
        }

        #endregion
    }

    [ContractClassFor(typeof(IGuestParticipation))]
    abstract class GuestParticipationContract : IGuestParticipation
    {
        #region IGuestParticipation Members

        public abstract int Id { get; }
        public abstract string Name { get; }

        public abstract IGuest Guest { get; }
        public abstract bool HasParticipated { get; }

        public void Update(bool partecipated)
        {
            Contract.Ensures(HasParticipated == partecipated);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Guest != null);
            Contract.Invariant(Guest.Id == Id && Guest.Name == Name);
        }
    }

    [ContractClassFor(typeof(IGuestParticipations))]
    abstract class GuestParticipationsContract : IGuestParticipations
    {
        #region IGuestParticipations Members

        public abstract IEnumerator<IGuestParticipation> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IGuestParticipation LastAdded { get; }
        public abstract IEnumerable<IGuestParticipation> Unordered { get; }
        public abstract IGuestParticipation this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract IGuestParticipation this[string name] { get; }
        public abstract bool Contains(string name);
        public abstract void Remove(string name);

        public IGuestParticipation Add(string guestName)
        {
            Contract.Requires(Manager.Guests.Contains(guestName) && !Contains(guestName));
            Contract.Ensures(LastAdded.Guest.Name == guestName.ToKey() && LastAdded.HasParticipated);
            return default(IGuestParticipation);
        }

        #endregion
    }

    [ContractClassFor(typeof(IIngredient))]
    abstract class IngredientContract : IIngredient
    {
        #region IIngredient Members

        public abstract int Id { get; }
        public abstract string Name { get; }
        public abstract bool Equals(IIngredient other);

        public abstract ILink<ICategory> Categories { get; }
        public abstract IEnumerable<IGuest> GuestIntolerances { get; }
        public abstract IEnumerable<IOtherRating<IGuest, FoodRating>> GuestRatings { get; }
        public abstract MeasureType MeasureType { get; }
        public abstract IEnumerable<IRecipe> OriginalRecipes { get; }
        public abstract IEnumerable<IRecipe> Recipes { get; }
        public abstract IEnumerable<IOtherRating<IShop, ShopRating>> ShopRatings { get; }
        public abstract IMeasure StockMeasure { get; }
        public abstract double StockQuantity { get; }

        public void Update(string name, MeasureType measureType, string stockMeasureName, double stockQuantity)
        {
            Contract.Requires(Manager.Measures.Contains(stockMeasureName));
            Contract.Requires<DataException>(stockQuantity >= 0, ErrorMessages.NegativeQuantity);
            ContractAbbreviators.RequireUnusedName(Name, name, Manager.Ingredients,
                                                   ErrorMessages.AlreadyUsedIngredientName);
            Contract.Ensures(Name == name.ToKey() && MeasureType == measureType &&
                             StockMeasure.Name == stockMeasureName.ToKey() && StockQuantity.Equals(stockQuantity));
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(StockMeasure != null && StockQuantity >= 0);
            Contract.Invariant(GuestIntolerances != null && GuestRatings != null);
            Contract.Invariant(GuestIntolerances.All(g => g.IngredientIntolerances.Contains(Id)));
            Contract.Invariant(GuestRatings.All(g => g.Entity.IngredientRatings.Contains(Id)));
            Contract.Invariant(Categories != null && ShopRatings != null);
            Contract.Invariant(Categories.All(c => c.Ingredients.Contains(Id)));
            Contract.Invariant(ShopRatings.All(s => s.Entity.IngredientRatings.Contains(Id)));
            Contract.Invariant(Recipes != null && OriginalRecipes != null);
            Contract.Invariant(Recipes.All(r => r.Ingredients.Contains(Id)));
            Contract.Invariant(OriginalRecipes.All(r => r.OriginalIngredients.Any(i => i.Id == Id)));
        }
    }

    [ContractClassFor(typeof(IIngredients))]
    abstract class IngredientsContract : IIngredients
    {
        #region IIngredients Members

        public abstract IEnumerator<IIngredient> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IIngredient LastAdded { get; }
        public abstract IEnumerable<IIngredient> Unordered { get; }
        public abstract IIngredient this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract IIngredient this[string id] { get; }
        public abstract bool Contains(string id);
        public abstract void Remove(string name);

        public IIngredient Add(string name, MeasureType type, string stockMeasureName, double stockQuantity)
        {
            Contract.Requires(Manager.Measures.Contains(stockMeasureName));
            Contract.Requires<DataException>(!Contains(name), ErrorMessages.AlreadyUsedIngredientName);
            Contract.Requires<DataException>(stockQuantity >= 0, ErrorMessages.NegativeQuantity);
            ContractAbbreviators.EnsureValidNamedEntitiesAdd(this, name);
            Contract.Ensures(Contract.Result<IIngredient>().MeasureType == type);
            Contract.Ensures(Contract.Result<IIngredient>().StockMeasure.Name == stockMeasureName.ToKey());
            Contract.Ensures(Contract.Result<IIngredient>().StockQuantity.Equals(stockQuantity));
            return default(IIngredient);
        }

        #endregion
    }

    [ContractClassFor(typeof(IIngredientQuantity))]
    abstract class IngredientQuantityContract : IIngredientQuantity
    {
        #region IIngredientQuantity Members

        public abstract int Id { get; }
        public abstract string Name { get; }

        public abstract string FormattedQuantity { get; }
        public abstract IIngredient Ingredient { get; }
        public abstract IMeasure Measure { get; }
        public abstract string Notes { get; }
        public abstract double Quantity { get; }

        public void Update(string measureName, double quantity, string notes)
        {
            Contract.Requires(Manager.Measures.Contains(measureName) && notes != null);
            Contract.Requires<DataException>(quantity > 0, ErrorMessages.NegativeOrZeroQuantity);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Ingredient != null && Measure != null && Notes != null && Quantity > 0);
            Contract.Invariant(!string.IsNullOrEmpty(FormattedQuantity));
        }
    }

    [ContractClassFor(typeof(IIngredientQuantities))]
    abstract class IngredientQuantitiesContract : IIngredientQuantities
    {
        #region IIngredientQuantities Members

        public abstract IEnumerator<IIngredientQuantity> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IIngredientQuantity LastAdded { get; }
        public abstract IEnumerable<IIngredientQuantity> Unordered { get; }
        public abstract IIngredientQuantity this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract IIngredientQuantity this[string name] { get; }
        public abstract bool Contains(string name);
        public abstract void Remove(string name);

        public IIngredientQuantity Add(string name, string measureName, double quantity, string notes)
        {
            Contract.Requires(notes != null && Manager.Measures.Contains(measureName));
            Contract.Requires(Manager.Ingredients.Contains(name) && !Contains(name));
            Contract.Requires<DataException>(quantity > 0, ErrorMessages.NegativeOrZeroQuantity);
            ContractAbbreviators.EnsureValidNamedEntitiesAdd(this, name);
            Contract.Ensures(Contract.Result<IIngredientQuantity>().Measure.Name == measureName.ToKey());
            Contract.Ensures(Contract.Result<IIngredientQuantity>().Quantity.Equals(quantity));
            Contract.Ensures(Contract.Result<IIngredientQuantity>().Notes == notes);
            return default(IIngredientQuantity);
        }

        #endregion
    }

    [ContractClassFor(typeof(IMeasure))]
    abstract class MeasureContract : IMeasure
    {
        #region IMeasure Members

        public abstract int Id { get; }
        public abstract string Name { get; }
        public abstract bool Equals(IMeasure other);

        public abstract double ConversionFactor { get; }
        public abstract MeasureFamily Family { get; }
        public abstract string ShortName { get; }
        public abstract MeasureType Type { get; }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(ConversionFactor > 0 && ShortName != null);
        }
    }

    [ContractClassFor(typeof(IMeasures))]
    abstract class MeasuresContract : IMeasures
    {
        #region IMeasures Members

        public abstract IEnumerator<IMeasure> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IMeasure LastAdded { get; }
        public abstract IEnumerable<IMeasure> Unordered { get; }
        public abstract IMeasure this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract IMeasure this[string name] { get; }
        public abstract bool Contains(string name);
        public abstract void Remove(string name);

        public IMeasure Add(string name, string shortName, MeasureType type, MeasureFamily family,
                            double conversionFactor)
        {
            Contract.Requires(!Contains(name) && shortName != null && conversionFactor > 0);
            ContractAbbreviators.EnsureValidNamedEntitiesAdd(this, name);
            Contract.Ensures(Contract.Result<IMeasure>().ShortName == shortName);
            Contract.Ensures(Contract.Result<IMeasure>().Type == type);
            Contract.Ensures(Contract.Result<IMeasure>().Family == family);
            Contract.Ensures(Contract.Result<IMeasure>().ConversionFactor.Equals(conversionFactor));
            return default(IMeasure);
        }

        #endregion
    }

    [ContractClassFor(typeof(IRecipe))]
    abstract class RecipeContract : IRecipe
    {
        #region IRecipe Members

        public abstract int Id { get; }
        public abstract string Name { get; }
        public abstract bool Equals(IRecipe other);

        public abstract IEnumerable<IEvent> Events { get; }
        public abstract IEnumerable<IOtherRating<IGuest, FoodRating>> GuestRatings { get; }
        public abstract bool HasOriginal { get; }
        public abstract IIngredientQuantities Ingredients { get; }
        public abstract MeasureFamily MeasureFamily { get; }
        public abstract IEnumerable<IIngredientQuantity> OriginalIngredients { get; }
        public abstract int? OriginalPrepHours { get; }
        public abstract int? OriginalPrepMinutes { get; }
        public abstract int? OriginalServings { get; }
        public abstract IEnumerable<IRecipeStep> OriginalSteps { get; }
        public abstract int? PrepHours { get; }
        public abstract int? PrepMinutes { get; }
        public abstract int? Servings { get; }
        public abstract string Source { get; }
        public abstract IRecipeSteps Steps { get; }
        public abstract IEnumerable<IRecipe> SubRecipeOf { get; }
        public abstract IRecipeTrials Trials { get; }

        public void MakeOriginal()
        {
            Contract.Ensures(HasOriginal && OriginalServings == Servings);
            Contract.Ensures(OriginalPrepHours == PrepHours && OriginalPrepMinutes == PrepMinutes);
            Contract.Ensures(OriginalIngredients.All(i => Ingredients.Contains(i.Id)));
        }

        public void Update(string name, string source, MeasureFamily measureFamily, int? prepHours, int? prepMinutes,
                           int? servings)
        {
            Contract.Requires(name != null && source != null);
            Contract.Requires<DataException>(Name.ToLower() == name.ToLower() || !Manager.Recipes.Contains(name),
                                             ErrorMessages.AlreadyUsedRecipeName);
            ContractAbbreviators.RequireValidRecipeInfo(prepHours, prepMinutes, servings);
            Contract.Ensures(Source == source && PrepHours == prepHours && PrepMinutes == prepMinutes &&
                             Servings == servings);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Ingredients != null && OriginalIngredients != null);
            Contract.Invariant(Ingredients.All(i => i.Ingredient.Recipes.Any(r => r.Id == Id)));
            Contract.Invariant(OriginalIngredients.All(i => i.Ingredient.Recipes.Any(r => r.Id == Id)));
            Contract.Invariant(Steps != null && OriginalSteps != null);
            Contract.Invariant(Steps.All(s => s.Recipe.Id == Id));
            Contract.Invariant(OriginalSteps.All(s => s.Recipe.Id == Id));
            Contract.Invariant(Source != null && Trials != null);
            Contract.Invariant(Trials.All(t => t.Recipe.Id == Id));
            Contract.Invariant(GuestRatings != null && SubRecipeOf != null && Events != null);
            Contract.Invariant(GuestRatings.All(g => g.Entity.RecipeRatings.Any(r => r.Id == Id)));
            Contract.Invariant(SubRecipeOf.All(r => r.Steps.Any(s => s.SubRecipe.Id == Id) ||
                                                    r.OriginalSteps.Any(s => s.SubRecipe.Id == Id)));
            Contract.Invariant(Events.All(e => e.Recipes.Any(r => r.Id == Id)));
        }
    }

    [ContractClassFor(typeof(IRecipes))]
    abstract class RecipesContract : IRecipes
    {
        #region IRecipes Members

        public abstract IEnumerator<IRecipe> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IRecipe LastAdded { get; }
        public abstract IEnumerable<IRecipe> Unordered { get; }
        public abstract IRecipe this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract IRecipe this[string id] { get; }
        public abstract bool Contains(string id);
        public abstract void Remove(string name);

        public IRecipe Add(string name, string source, MeasureFamily measureFamily, int? prepHours, int? prepMinutes,
                           int? servings)
        {
            Contract.Requires(source != null);
            Contract.Requires<DataException>(!Contains(name), ErrorMessages.AlreadyUsedRecipeName);
            ContractAbbreviators.RequireValidRecipeInfo(prepHours, prepMinutes, servings);
            ContractAbbreviators.EnsureValidNamedEntitiesAdd(this, name);
            Contract.Ensures(Contract.Result<IRecipe>().Source == source &&
                             Contract.Result<IRecipe>().MeasureFamily == measureFamily &&
                             Contract.Result<IRecipe>().PrepHours == prepHours &&
                             Contract.Result<IRecipe>().PrepMinutes == prepMinutes &&
                             Contract.Result<IRecipe>().Servings == servings);
            return default(IRecipe);
        }

        #endregion
    }

    [ContractClassFor(typeof(IRecipeServings))]
    abstract class RecipeServingsContract : IRecipeServings
    {
        #region IRecipeServings Members

        public abstract int Id { get; }
        public abstract string Name { get; }

        public abstract IRecipe Recipe { get; }
        public abstract int? Servings { get; }

        public void Update(int? servings)
        {
            ContractAbbreviators.RequireValidRecipeInfo(servings);
            Contract.Ensures(Servings == servings);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Recipe != null);
            Contract.Invariant(Recipe.Id == Id && Recipe.Name == Name);
        }
    }

    [ContractClassFor(typeof(IRecipesServings))]
    abstract class RecipesServingsContract : IRecipesServings
    {
        #region IRecipesServings Members

        public abstract IEnumerator<IRecipeServings> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IRecipeServings LastAdded { get; }
        public abstract IEnumerable<IRecipeServings> Unordered { get; }
        public abstract IRecipeServings this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract IRecipeServings this[string name] { get; }
        public abstract bool Contains(string name);
        public abstract void Remove(string name);

        public IRecipeServings Add(string recipeName, int? servings)
        {
            Contract.Requires(Manager.Recipes.Contains(recipeName));
            ContractAbbreviators.RequireValidRecipeInfo(servings);
            Contract.Ensures(LastAdded.Recipe.Name == recipeName.ToKey());
            Contract.Ensures(LastAdded.Servings == (servings ?? LastAdded.Recipe.Servings));
            return default(IRecipeServings);
        }

        #endregion
    }

    [ContractClassFor(typeof(IRecipeStat))]
    abstract class RecipeStatContract : IRecipeStat
    {
        #region IRecipeStat Members

        public abstract int Id { get; }
        public abstract string Name { get; }

        public abstract int Count { get; }
        public abstract IRecipe Recipe { get; }
        public abstract DateTime LastServed { get; }

        public void Update(DateTime newDate)
        {
            Contract.Ensures(Count == Contract.OldValue(Count) + 1 &&
                             ((Contract.OldValue(LastServed) < newDate && LastServed == newDate) ||
                              LastServed == Contract.OldValue(LastServed)));
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Count > 0 && Recipe != null);
            Contract.Invariant(Recipe.Id == Id && Recipe.Name == Name);
        }
    }

    [ContractClassFor(typeof(IRecipeStats))]
    abstract class RecipeStatsContract : IRecipeStats
    {
        #region IRecipeStats Members

        public abstract IEnumerator<IRecipeStat> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IRecipeStat LastAdded { get; }
        public abstract IEnumerable<IRecipeStat> Unordered { get; }
        public abstract IRecipeStat this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract IRecipeStat this[string name] { get; }
        public abstract bool Contains(string name);
        public abstract void Remove(string name);

        public IRecipeStat Add(string recipeName, DateTime lastServed)
        {
            Contract.Requires(Manager.Recipes.Contains(recipeName));
            Contract.Ensures(LastAdded.Recipe.Name == recipeName.ToKey() && LastAdded.LastServed == lastServed);
            return default(IRecipeStat);
        }

        #endregion
    }

    [ContractClassFor(typeof(IRecipeStep))]
    abstract class RecipeStepContract : IRecipeStep
    {
        #region IRecipeStep Members

        public abstract int Id { get; }

        public string Description
        {
            get
            {
                Contract.Ensures((Type == StepType.SubRecipe && Contract.Result<string>() == SubRecipe.Name) ||
                                 (Type == StepType.Generic && Contract.Result<string>() != null &&
                                  Contract.Result<string>().Length > 0));
                return default(string);
            }
        }

        public abstract IRecipe Recipe { get; }
        public abstract string Resources { get; }
        public abstract int? Servings { get; }
        public abstract int? StepHours { get; }
        public abstract int? StepMinutes { get; }
        public abstract IRecipe SubRecipe { get; }
        public abstract StepType Type { get; }

        public void Update(string description, string resources, int? stepHours, int? stepMinutes)
        {
            Contract.Requires(description != null && resources != null);
            Contract.Requires<DataException>(description.Length > 0, ErrorMessages.ZeroLengthDescription);
            ContractAbbreviators.RequireValidRecipeInfo(stepHours, stepMinutes);
            Contract.Ensures(Type == StepType.Generic && Description == description && Resources == resources &&
                             StepHours == stepHours && StepMinutes == stepMinutes);
        }

        public void Update(string subRecipeName, int? servings)
        {
            Contract.Requires(Manager.Recipes.Contains(subRecipeName));
            ContractAbbreviators.RequireValidRecipeInfo(servings);
            Contract.Ensures(Type == StepType.SubRecipe && SubRecipe.Name == subRecipeName.ToKey() &&
                             Servings == servings);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Resources != null);
            Contract.Invariant(Recipe != null);
            Contract.Invariant(Recipe.Steps.Contains(Id) || Recipe.OriginalSteps.Any(s => s.Id == Id));
            Contract.Invariant(Type == StepType.Generic || StepHours == SubRecipe.PrepHours);
            Contract.Invariant(Type == StepType.Generic || StepMinutes == SubRecipe.PrepMinutes);
            Contract.Invariant(SubRecipe == null || SubRecipe.SubRecipeOf.Any(r => r.Id == Recipe.Id));
        }
    }

    [ContractClassFor(typeof(IRecipeSteps))]
    abstract class RecipeStepsContract : IRecipeSteps
    {
        #region IRecipeSteps Members

        public abstract IEnumerator<IRecipeStep> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IRecipeStep LastAdded { get; }
        public abstract IEnumerable<IRecipeStep> Unordered { get; }
        public abstract IRecipeStep this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);

        public IRecipeStep AddGeneric(string description, string resources, int? stepHours, int? stepMinutes)
        {
            Contract.Requires(description != null && resources != null);
            Contract.Requires<DataException>(description.Length > 0, ErrorMessages.ZeroLengthDescription);
            ContractAbbreviators.RequireValidRecipeInfo(stepHours, stepMinutes);
            Contract.Ensures(Contract.Result<IRecipeStep>().Description == description &&
                             Contract.Result<IRecipeStep>().Resources == resources &&
                             Contract.Result<IRecipeStep>().StepHours == stepHours &&
                             Contract.Result<IRecipeStep>().StepMinutes == stepMinutes &&
                             Contract.Result<IRecipeStep>().Type == StepType.Generic &&
                             Count == Contract.OldValue(Count) + 1);
            return default(IRecipeStep);
        }

        public IRecipeStep AddSubRecipe(string subRecipeName, int? servings)
        {
            Contract.Requires(Manager.Recipes.Contains(subRecipeName));
            ContractAbbreviators.RequireValidRecipeInfo(servings);
            Contract.Ensures(Contract.Result<IRecipeStep>().SubRecipe.Name == subRecipeName.ToKey() &&
                             Contract.Result<IRecipeStep>().Servings == servings &&
                             Contract.Result<IRecipeStep>().Type == StepType.SubRecipe &&
                             Count == Contract.OldValue(Count) + 1);
            return default(IRecipeStep);
        }

        public void Clear()
        {
            Contract.Ensures(Count == 0);
        }

        #endregion
    }

    [ContractClassFor(typeof(IRecipeTrial))]
    abstract class RecipeTrialContract : IRecipeTrial
    {
        #region IRecipeTrial Members

        public abstract int Id { get; }

        public abstract string Notes { get; }
        public abstract IRecipe Recipe { get; }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Notes != null);
            Contract.Invariant(Recipe != null && Recipe.Trials.Contains(Id));
        }
    }

    [ContractClassFor(typeof(IRecipeTrials))]
    abstract class RecipeTrialsContract : IRecipeTrials
    {
        #region IRecipeTrials Members

        public abstract IEnumerator<IRecipeTrial> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IRecipeTrial LastAdded { get; }
        public abstract IEnumerable<IRecipeTrial> Unordered { get; }
        public abstract IRecipeTrial this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);

        public IRecipeTrial Add(string notes)
        {
            Contract.Requires(notes != null);
            ContractAbbreviators.EnsureValidEntitiesAdd(this);
            Contract.Ensures(Contract.Result<IRecipeTrial>().Notes == notes);
            return default(IRecipeTrial);
        }

        #endregion
    }

    [ContractClassFor(typeof(IShop))]
    abstract class ShopContract : IShop
    {
        #region IShop Members

        public abstract int Id { get; }
        public abstract string Name { get; }
        public abstract bool Equals(IShop other);

        public abstract string Address { get; }
        public abstract string City { get; }
        public abstract string PhoneNumber { get; }
        public abstract string Timetable { get; }
        public abstract IRatings<IIngredient, ShopRating> IngredientRatings { get; }

        public void Update(string name, string address, string city, string phoneNumber, string timetable)
        {
            Contract.Requires(address != null && city != null && phoneNumber != null && timetable != null);
            ContractAbbreviators.RequireUnusedName(Name, name, Manager.Shops, ErrorMessages.AlreadyUsedShopName);
            Contract.Ensures(Name == name.ToKey() && Address == address && City == city && PhoneNumber == phoneNumber &&
                             Timetable == timetable);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Address != null && City != null);
            Contract.Invariant(PhoneNumber != null && Timetable != null);
            Contract.Invariant(IngredientRatings != null);
            Contract.Invariant(IngredientRatings.All(i => i.Entity.ShopRatings.Any(s => s.Id == Id)));
        }
    }

    [ContractClassFor(typeof(IShops))]
    abstract class ShopsContract : IShops
    {
        #region IShops Members

        public abstract IEnumerator<IShop> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }
        public abstract IShop LastAdded { get; }
        public abstract IEnumerable<IShop> Unordered { get; }
        public abstract IShop this[int id] { get; }
        public abstract bool Contains(int id);
        public abstract void Remove(int id);
        public abstract IShop this[string name] { get; }
        public abstract bool Contains(string name);
        public abstract void Remove(string name);

        public IShop Add(string name, string address, string city, string timetable, string phoneNumber)
        {
            Contract.Requires(address != null && city != null && timetable != null && phoneNumber != null);
            Contract.Requires<DataException>(!Contains(name), ErrorMessages.AlreadyUsedShopName);
            ContractAbbreviators.EnsureValidNamedEntitiesAdd(this, name);
            Contract.Ensures(Contract.Result<IShop>().Address == address && Contract.Result<IShop>().City == city &&
                             Contract.Result<IShop>().Timetable == timetable &&
                             Contract.Result<IShop>().PhoneNumber == phoneNumber);
            return default(IShop);
        }

        #endregion
    }

    [ContractClassFor(typeof(IShoppingList))]
    abstract class ShoppingListContract : IShoppingList
    {
        #region IShoppingList Members

        public abstract IEnumerator<IIngredientQuantity> GetEnumerator();

        IEnumerator IEnumerable.GetEnumerator()
        {
            return GetEnumerator();
        }

        public abstract int Count { get; }

        public IIngredientQuantity this[string ingredientName, string measureName]
        {
            get
            {
                Contract.Requires(Contains(ingredientName, measureName));
                Contract.Ensures(Contract.Result<IIngredientQuantity>() != null &&
                                 Contract.Result<IIngredientQuantity>().Ingredient.Name == ingredientName.ToKey() &&
                                 Contract.Result<IIngredientQuantity>().Measure.Name == measureName.ToKey() &&
                                 Contract.OldValue(Count) == Count);
                return default(IIngredientQuantity);
            }
        }

        public IIngredientQuantity Add(string ingredientName, string measureName, double quantity, string notes)
        {
            Contract.Requires(notes != null);
            Contract.Requires(Manager.Ingredients.Contains(ingredientName));
            Contract.Requires(Manager.Measures.Contains(measureName));
            Contract.Requires<DataException>(measureName != "Quanto Basta", ErrorMessages.InvalidQbMeasure);
            Contract.Requires<DataException>(quantity > 0, ErrorMessages.NegativeOrZeroQuantity);
            Contract.Ensures(Contract.Result<IIngredientQuantity>() != null &&
                             Contract.Result<IIngredientQuantity>().Ingredient.Name == ingredientName.ToKey() &&
                             Contract.Result<IIngredientQuantity>().Notes == notes);
            Contract.Ensures(Contract.Result<IIngredientQuantity>().Measure.Name == "Grammi" ||
                             Contract.Result<IIngredientQuantity>().Measure.Name == "Litri" ||
                             Contract.Result<IIngredientQuantity>().Measure.Name == "Unità");
            Contract.Ensures(Count == Contract.OldValue(Count) || Count == Contract.OldValue(Count) + 1);
            return default(IIngredientQuantity);
        }

        public void Clear()
        {
            Contract.Ensures(Count == 0);
        }

        public bool Contains(string ingredientName, string measureName)
        {
            Contract.Requires(ingredientName != null && measureName != null);
            Contract.Ensures(Contract.OldValue(Count) == Count);
            return default(bool);
        }

        public void Remove(string ingredientName, string measureName)
        {
            Contract.Requires(Contains(ingredientName, measureName));
            Contract.Ensures(!Contains(ingredientName, measureName) && Contract.OldValue(Count) - 1 == Count);
        }

        #endregion

        [ContractInvariantMethod]
        void Invariant()
        {
            Contract.Invariant(Count >= 0);
        }
    }

// ReSharper disable UnusedParameter.Global
    static class ContractAbbreviators
    {
        [ContractAbbreviator]
        public static void EnsureValidEntitiesAdd<TEntity>(IEntities<TEntity> entities)
            where TEntity : class, IEntity
        {
            Contract.Ensures(Contract.Result<TEntity>() != null);
            Contract.Ensures(entities.Contains(Contract.Result<TEntity>().Id) &&
                             entities.Count == Contract.OldValue(entities.Count) + 1);
        }

        [ContractAbbreviator]
        public static void EnsureValidNamedEntitiesAdd<TEntity>(INamedEntities<TEntity> entities, string name)
            where TEntity : class, INamedEntity
        {
            EnsureValidEntitiesAdd(entities);
            Contract.Ensures(entities.Contains(Contract.Result<TEntity>().Name));
            Contract.Ensures(Contract.Result<TEntity>().Name == name.ToKey());
        }

        [ContractAbbreviator]
        public static void RequireUnusedName<TEntity>(string currName, string newName, INamedEntities<TEntity> entities,
                                                      string message)
            where TEntity : class, INamedEntity
        {
            Contract.Requires<DataException>(currName.ToLower() == newName.ToLower() ||
                                             !entities.Contains(newName), message);
        }

        [ContractAbbreviator]
        public static void RequireValidName(string name)
        {
            Contract.Requires(name != null);
            Contract.Requires<DataException>(name.Length > 0, ErrorMessages.ZeroLengthName);
        }

        [ContractAbbreviator]
        public static void RequireValidRecipeInfo(int? hours, int? minutes, int? servings)
        {
            Contract.Requires<DataException>(hours == null || hours >= Settings.Default.MinHours &&
                                             hours <= Settings.Default.MaxHours, ErrorMessages.InvalidHours);
            Contract.Requires<DataException>(minutes == null || minutes >= Settings.Default.MinMinutes &&
                                             minutes <= Settings.Default.MaxMinutes, ErrorMessages.InvalidMinutes);
            Contract.Requires<DataException>(servings == null || servings >= Settings.Default.MinServings &&
                                             servings <= Settings.Default.MaxServings, ErrorMessages.InvalidServings);
        }

        [ContractAbbreviator]
        public static void RequireValidRecipeInfo(int? hours, int? minutes)
        {
            Contract.Requires<DataException>(hours == null || hours >= Settings.Default.MinHours &&
                                             hours <= Settings.Default.MaxHours, ErrorMessages.InvalidHours);
            Contract.Requires<DataException>(minutes == null || minutes >= Settings.Default.MinMinutes &&
                                             minutes <= Settings.Default.MaxMinutes, ErrorMessages.InvalidMinutes);
        }

        [ContractAbbreviator]
        public static void RequireValidRecipeInfo(int? servings)
        {
            Contract.Requires<DataException>(servings == null || servings >= Settings.Default.MinServings &&
                                             servings <= Settings.Default.MaxServings, ErrorMessages.InvalidServings);
        }
    }

// ReSharper restore UnusedParameter.Global

    [AttributeUsage(AttributeTargets.Method, AllowMultiple = false)]
    [Conditional("CONTRACTS_FULL")]
    sealed class ContractAbbreviatorAttribute : Attribute
    {
    }
}